\begin{tabbing}
dt($l$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$compose{-}fpf($\lambda$$k$.\=if isrcv($k$)$\rightarrow$ if lnk($k$) = $l$$\rightarrow$ inl(tag($k$)) else inr($\cdot$) fi\+
\\[0ex]else inr($\cdot$) fi;$\lambda$${\it tg}$.rcv($l$,${\it tg}$);${\it da}$)
\-
\end{tabbing}